Durant quatre semaines, Google DeepMind a utilisé une nouvelle IA pour vérifier plusieurs garanties cryptographiques du protocole Signal. Une expérience qui pourrait changer la manière dont les chercheurs contrôlent la sécurité des logiciels.
On peut tester un programme des milliers de fois sans avoir exploré tous les scénarios possibles. Alors comment s’assurer qu’il respecte bien les garanties de sécurité qu’on attend de lui ? En produisant des preuves mathématiques. C’est le principe de la vérification formelle, une méthode qui existe depuis longtemps. Sauf que ces démonstrations représentent une somme de travail considérable. Google DeepMind a donc voulu savoir si l’IA pouvait accélérer les choses, en choisissant un terrain d’essai de taille : le protocole de chiffrement Signal, utilisé pour protéger les communications de Signal, WhatsApp et Google Messages.
Protégez votre entreprise gratuitement pendant 30 jours
Découvrez Bitdefender Ultimate Small Business Security et protégez votre activité contre les cybermenaces. Aucune coordonnée bancaire requise.
Le protocole Signal à l’épreuve d’AlphaProof Code
Pour relever le défi, les chercheurs ont utilisé AlphaProof Code, un nouveau système reposant sur des agents IA capables de participer à la construction de démonstrations mathématiques. Leur mission n’était pas de chercher des failles dans Signal, mais d’aider à prouver que plusieurs propriétés de son chiffrement étaient bien respectées, y compris dans le code chargé de les appliquer. Car un protocole peut être correctement conçu sur le plan théorique et présenter malgré tout des erreurs dans son implémentation.
DeepMind a donc travaillé sur une version compilée de libsignal, la bibliothèque de référence du protocole, pour pousser les vérifications jusqu’au code machine. Les agents chargés des preuves, reposant sur Gemini 4 Carbon, ont pu explorer différentes pistes, revenir sur leurs erreurs et ajuster leurs raisonnements, sous la supervision des chercheurs aux étapes décisives. Les preuves obtenues ont ensuite été contrôlées par Lean, un logiciel capable d’en vérifier la validité mathématique.
Les résultats se sont révélés encourageants. Selon WIRED, il n’a fallu que quatre semaines à DeepMind pour démontrer plusieurs garanties cryptographiques essentielles du protocole, parmi lesquelles la confidentialité des messages, l’authentification des correspondants et certaines protections en cas de compromission des clés, sans découvrir de nouvelle vulnérabilité dans les parties examinées.
Pour pousser l’expérience plus loin, l’équipe a ensuite réintroduit dans le code de Signal deux anciennes vulnérabilités, corrigées depuis longtemps. L’outil a alors permis de démontrer mathématiquement que les versions ainsi modifiées ne respectaient plus les garanties de sécurité examinées.
Les chercheurs ont néanmoins bénéficié d’un point de départ précieux. Des travaux de vérification formelle existaient déjà sur certaines parties du protocole Signal. DeepMind a donc pu s’appuyer sur ces analyses pour étendre les démonstrations à son implémentation, jusqu’alors beaucoup plus difficile à vérifier.
Une avancée prometteuse, mais pas un certificat de sécurité universel
Il serait toutefois exagéré d’en conclure que Google a mathématiquement prouvé l’absence de vulnérabilités dans Signal. La vérification formelle porte sur des propriétés précises, dans un cadre défini à l’avance, et dépend des hypothèses retenues pour construire les preuves. Dans le cas de Signal, les chercheurs ont notamment supposé que certaines fonctions cryptographiques étaient sûres, sans vérifier directement leur code. Une preuve valide garantit donc le respect des propriétés examinées dans ces conditions, mais ne dit rien des éventuelles failles dans les fonctions qui n’ont pas été analysées.
Les chercheurs n'ont d’ailleurs pas vérifié l’application Signal dans son ensemble. Leurs démonstrations concernent les échanges individuels, sans couvrir les conversations de groupe ni les usages sur plusieurs appareils. Certaines garanties de résistance aux attaques quantiques restent également en dehors du périmètre vérifié. Ils n'ont pas non plus examiné WhatsApp ou Google Messages, même si les deux messageries utilisent ce protocole pour chiffrer leurs échanges.
Les chercheurs de DeepMind espèrent désormais utiliser cette méthode pour contrôler des logiciels entiers, ainsi que les programmes et bibliothèques dont ils dépendent. De telles preuves pourraient ainsi servir aux banques et aux organisations qui exploitent des systèmes critiques pour confirmer mathématiquement le respect d’exigences de sécurité précises. Mais cela suppose qu’AlphaProof Code puisse examiner des logiciels beaucoup plus volumineux, ce qui reste à démontrer. Google n’a pas non plus communiqué le coût de l’expérience menée sur Signal, ni même indiqué si l’outil pourrait un jour être proposé aux entreprises.
Les spécifications et les preuves produites durant ces quatre semaines ont toutefois été publiées en accès libre. D’autres équipes peuvent désormais les examiner, reproduire les vérifications et évaluer plus précisément la portée des résultats annoncés par DeepMind.
